Proving probabilistic noninterference
Dr. Andrei Popescu 	

We introduce a series of bisimilarity relations on the Markov chain associated to a 
simple probabilistic programming language. These  bisimilarities are used to ensure, 
via suitable type systems, various degrees of noninterference, expressed as 
probabilistic properties on execution traces.  

This is joint work at TUM with Johannes Hoelzl and Tobias Nipkow.